h-ordered(es;e.P(e);H)
== e:{e:E| P(e)} .
== (e  H(e))
== & (e':{e:E| P(e)} .
== & ((e c e'  (e  H(e')))
== & (& ((e  H(e'))  (e'  H(e)))
== & (& ((e  H(e'))  (e'  H(e))  (e = e'))
== & (& ((e  H(e'))  H(e)  H(e'))) 

latex

---

clarification:

h-ordered(es;e.P(e);H)
== e:{e:es-E(es)| P(e)} .
== (e  H(e)  es-E(es))
== & (e':{e:es-E(es)| P(e)} .
== & ((es-causle(es;e;e')  (e  H(e')  es-E(es)))
== & (& ((e  H(e')  es-E(es))  (e'  H(e)  es-E(es)))
== & (& ((e  H(e')  es-E(es))  (e'  H(e)  es-E(es))  (e = e'  es-E(es)))
== & (& ((e  H(e')  es-E(es))  H(e)  H(e')  es-E(es) List)) 

latex

Definitions	x:A. B(x), {x:A| B(x)} , e c e', P  Q, P & Q, s = t, P  Q, (x  l), l1  l2, E, f(a)
FDL editor aliases	h-ordered